n:, i:{0...n}. choose(n;i)   

latex

Up	rings 1
Definitions of Statement	choose(n;i)
Definitions	t  T, x:A. B(x), False, A, A  B, i  j , P  Q, True, T, ff, P  Q, , P  Q, P  Q, tt, P & Q, if b then t else f fi , Y, choose(n;i), , {i...j}, Unit, ,
Lemmas	nat wf, le wf, nat properties, assert of eq int, not functionality wrt iff, assert of bnot, and functionality wrt iff, assert of band, bnot thru bor, true wf, squash wf, eqff to assert, not wf, bnot wf, band wf, assert of bor, eqtt to assert, assert wf, iff transitivity, bool wf, eq int wf, bor wf, add nat wf